enrich
   encoding-nat
, 
   encoding-volid
, 
   vtbl, 
   nat-mult

with
   

   
   
   
   predicates  is-encoded : vtbl × buffer;
               is-encoded-rec : vtbl × buffer;
   procedures encode_vtbl#  : vtbl × buffer : error  nondeterministic;
              decode_vtbl# buffer :  : vtbl × error  nondeterministic;
   variables  INDEX : nat flexible;
              SIZE : nat flexible;
              N : nat flexible;
              M : nat flexible;
              VTBL : vtbl flexible;
              ERR : error flexible;
              BUF : buffer flexible;
              VOLID : volid flexible;
   
   

   

   axioms is-encoded
          :  ⊦ is-encoded(vtbl, buf) ↔ (∃ buf0, buf1, buf2. buf = buf0 + buf1 + buf2 ∧ is-encoded(# vtbl, buf0) ∧ is-encoded-rec(vtbl, buf1));
          is-encoded-base :  ⊦ is-encoded-rec(∅, buf) ↔ # buf = 0;
          used for: s, ls;
          is-encoded-rec
          : vtbl ≠ ∅
            ⊦   is-encoded-rec(vtbl, buf)
              ↔ (∃ v, buf0, buf1, buf2. 
                   v ∈ vtbl ∧ buf = buf0 + buf1 + buf2 ∧ is-encoded(v, buf0) ∧ is-encoded(vtbl[v], buf1) ∧ is-encoded-rec(vtbl -- v, buf2));

   

   declarations encode-vtbl
                : encode_vtbl#(; VTBL, BUF; ERR)
                  {ERR := ESUCCESS; 
                   let INDEX = 0, SIZE = ?
                   in {encode_nat#(# VTBL, INDEX; BUF, SIZE; ERR); INDEX := INDEX + SIZE; 
                       while ERR = ESUCCESS ∧ VTBL ≠ ∅
                       do {/* (encode
                               : invariant   (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ # BUF = # BUF`
                                           ∧ (  ERR = ESUCCESS
                                              → (∃ buf0, buf1, buf2, vtbl0. 
                                                     BUF = buf0 + buf1 + buf2 ∧ VTBL` = VTBL ∪ vtbl0 ∧ VTBL ⊥ vtbl0 ∧ # buf0 + # buf1 = INDEX
                                                   ∧ # buf2 ≥ # VTBL * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) ∧ is-encoded(# VTBL`, buf0)
                                                   ∧ is-encoded-rec(vtbl0, buf1)))
                               wfbound # VTBL)
                           */; 
                           choose VOLID
                           with VOLID ∈ VTBL
                           in {encode_volid#(VOLID, INDEX; BUF, SIZE; ERR); 
                               if ERR = ESUCCESS
                               then {INDEX := INDEX + SIZE; encode_nat#(VTBL[VOLID], INDEX; BUF, SIZE; ERR); INDEX := INDEX + SIZE}; 
                               VTBL := VTBL -- VOLID}}}
                  }
                ;
                decode-vtbl
                : decode_vtbl#(BUF; ; VTBL, ERR)
                  {VTBL := ∅; ERR := ESUCCESS; 
                   let N = ?, INDEX = 0, SIZE = ?
                   in {decode_nat#(INDEX, BUF; N, SIZE; ERR); INDEX := INDEX + SIZE; 
                       while N ≠ 0 ∧ ERR = ESUCCESS
                       do {/* (decode
                               : invariant   (ERR = ESUCCESS ∨ ⌊ERR⌋ )
                                           ∧ (  ERR = ESUCCESS
                                              → (∃ vtbl1. 
                                                     VTBL ⊥ vtbl1 ∧ # vtbl1 + # VTBL = N` ∧ # vtbl1 = N
                                                   ∧ # BUF ≥ ENCODED_NAT_SIZE + N` * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE)
                                                   ∧ INDEX = ENCODED_NAT_SIZE + # VTBL * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE)
                                                   ∧ is-encoded(N`, subarray(BUF, 0, ENCODED_NAT_SIZE))
                                                   ∧ is-encoded-rec
                                                     (VTBL, subarray(BUF, ENCODED_NAT_SIZE, # VTBL * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE)))
                                                   ∧ is-encoded-rec
                                                     (vtbl1, subarray(BUF, INDEX, # vtbl1 * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE)))))
                               wfbound N)
                           */; 
                           let VOLID = ?, M = ?
                           in {decode_volid#(INDEX, BUF; VOLID, SIZE; ERR); 
                               if ERR = ESUCCESS
                               then {INDEX := INDEX + SIZE; decode_nat#(INDEX, BUF; M, SIZE; ERR); 
                                     if ERR = ESUCCESS then {INDEX := INDEX + SIZE; VTBL[VOLID] := M}}}; 
                           N := N - 1}}
                  }
                ;
end enrich